(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(declare-fun x () (Nullable Int))
(declare-fun y () (Nullable Int))
(declare-fun z () (Nullable Int))
(assert (distinct x y z))
(assert (= x (as nullable.null (Nullable Int))))
(assert (= y (nullable.some 5)))
(check-sat)
